*****EVAL length qNIL=0 BY SEXPSS∪PROPSS∪{ LENGTH_DF};

1 length qNIL=0  

*****EVAL ∀uu.length uu=add1 length cdr uu BY SEXPSS∪PROPSS∪{ LENGTH_DF};

2 ∀uu.length uu=add1 length cdr uu  

*****LABEL I_LENUV;

*****∧I LISTINDUCTION;

3 (∀v.length (qNIL*v)=(length qNIL+length v)∧∀uu.(∀v.length (cdr uu*v)=(length cdr uu+length v)⊃∀v.length (uu*v)%
=(length uu+length v)))⊃∀u v.length (u*v)=(length u+length v)  

*****LABEL NIL_LENUV;

*****EVAL ∀v.length (qNIL*v)=(length qNIL+length v) BY ARITHSS∪{ APPEND_NIL,LENGTH_NIL};

4 ∀v.length (qNIL*v)=(length qNIL+length v)  

*****LABEL H_LENUV;

*****ASSUME ∀v.length (cdr uu*v)=(length cdr uu+length v);

5 ∀v.length (cdr uu*v)=(length cdr uu+length v)  (5)

*****REWRITE ∀v.length (uu*v)=(length uu+length v) BY ARITHSS∪SEXPSS∪{ LENGTH_UU,APPEND_UU_V,H_LENUV};

6 ∀v.length (uu*v)=(length uu+length v)  (5)

*****⊃I H_LENUV⊃↑;

7 ∀v.length (cdr uu*v)=(length cdr uu+length v)⊃∀v.length (uu*v)=(length uu+length v)  

*****∀I ↑ uu;

8 ∀uu.(∀v.length (cdr uu*v)=(length cdr uu+length v)⊃∀v.length (uu*v)=(length uu+length v))  

*****TAUT ∀u v.length (u*v)=(length u+length v) I_LENUV:NIL_LENUV,8;

9 ∀u v.length (u*v)=(length u+length v)  

*****LABEL I_LENREV;

*****∧I LISTINDUCTION;

10 (length reverse1 qNIL=length qNIL∧∀uu.(length reverse1 cdr uu=length cdr uu⊃length reverse1 uu=length uu))⊃∀u%
.length reverse1 u=length u  

*****LABEL NIL_LENREV;

*****EVAL length reverse1 qNIL=length qNIL BY { REVERSE1_NIL,LENGTH_NIL};

11 length reverse1 qNIL=length qNIL  

*****LABEL H_LENREV;

*****ASSUME length reverse1 cdr uu=length cdr uu;

12 length reverse1 cdr uu=length cdr uu  (12)

*****REWRITE length reverse1 uu=length uu BY SEXPSS∪ARITHSS∪{ LENGTH_UU,LENGTH_NIL,LENGTH_UV,REVERSE1_UU,H_LENRE%
V};

13 length reverse1 uu=length uu  (12)

*****⊃I H_LENREV⊃↑;

14 length reverse1 cdr uu=length cdr uu⊃length reverse1 uu=length uu  

*****∀I ↑ uu;

15 ∀uu.(length reverse1 cdr uu=length cdr uu⊃length reverse1 uu=length uu)  

*****TAUT ∀u.length reverse1 u=length u I_LENREV:NIL_LENREV,15;

16 ∀u.length reverse1 u=length u  

*****REWRITE ∀uu.¬(length uu=0) BY LOGICTREE∪{ LENGTH_UU,ADD1_NOT_ZERO};

17 ∀uu.¬(length uu=0)  

*****∀E ↑ u;

18 NELIST u⊃¬(length u=0)  

*****REWRITE ↑ BY SEXPSS;

19 ¬(u=qNIL)⊃¬(length u=0)  

*****ASSUME u=qNIL;

20 u=qNIL  (20)

*****REWRITE length u BY { LENGTH_NIL,20};

21 length u=0  (20)

*****⊃I ↑↑⊃↑;

22 u=qNIL⊃length u=0  

*****TAUT length u=0≡u=qNIL 19,22;

23 length u=0≡u=qNIL  

*****∧I ALL_U;

24 ((length qNIL=0≡qNIL=qNIL)∧∀uu.(length uu=0≡uu=qNIL))⊃∀u.(length u=0≡u=qNIL)  

*****REWRITE length qNIL=0≡qNIL=qNIL BY LOGICTREE∪{ LENGTH_NIL};

25 length qNIL=0≡qNIL=qNIL  

*****REWRITE ∀uu.(length uu=0≡uu=qNIL) BY SEXPSS∪{ LENGTH_UU,ADD1_NOT_ZERO};

26 ∀uu.(length uu=0≡uu=qNIL)  

*****TAUT ∀u.(length u=0≡u=qNIL) 24:26;

27 ∀u.(length u=0≡u=qNIL)